Nuprl Lemma : fifoDecodes_wf
11,40
postcript
pdf
es
:ES,
ff
:FIFO.
ff
.Decodes
i
:
ff
.C
e
:{
x
:E|
ff
.R(
i
,
x
)}
state@loc(
e
)
ff
.T
latex
Definitions
state@
i
,
{
x
:
A
|
B
(
x
)}
,
f
(
a
)
,
E
,
x
:
A
B
(
x
)
,
x
:
A
B
(
x
)
,
ff
.C
,
ff
.R
,
ff
.T
,
ff
.Decodes
,
let
a
,
b
,
c
,
d
,
e
,
f
,
g
=
u
in
v
(
a
;
b
;
c
;
d
;
e
;
f
;
g
)
,
FIFO
,
x
:
A
.
B
(
x
)
,
t
T
,
ES
Lemmas
event
system
wf
,
FIFO
wf
origin
es:ES, ff:FIFO. ff.Decodes 
i:ff.C
e:{x:E| ff.R(i,x)} state@loc(e)ff.T es:ES, ff:FIFO. ff.Decodes i:ff.Ce:{x:E| ff.R(i,x)} state@loc(e)ff.T B(x)
B(x)x:A. B(x) T